A:Realizer, i, x:Id, k:Knd, test:(State(R-state(A;i))Valtype(R-da(A;i);k)).
R-Feasible(A)
 ((x  dom(R-state(A;i))))
 (hasloc(k;i))
 ((write-restricted(A;i;k)))
 (y:Id. (y  dom(x :   R-state(A;i)))  ((read-restricted(A; i; y))))
 A || R-base-recognize(i;R-state(A;i);x;k;Valtype(R-da(A;i);k);test) 

latex

Definitions

, {T}, SQType(T), State(ds), x. t(x), Top, P & Q, t  T, R-base-recognize(i;ds;x;k;T;test), P  Q, x:A. B(x), P  Q, x(s), State(ds)

Lemmas

R-compat-self, R-compat-da2, Id sq, assert-hasloc, fpf-compatible-self, fpf-compatible-single2, fpf-sub-join-right, ma-state-subtype, Kind-deq wf, isrcv wf, fpf-single wf3, fpf-cap wf, fpf-cap-single-join, btrue wf, ifthenelse wf, Reffect-compat, Rframe-compat, rationals wf, bfalse wf, Rinit-compat, es realizer wf, Knd wf, bool wf, decl-state wf, R-Feasible wf, hasloc wf, write-restricted wf, read-restricted wf, not wf, fpf wf, fpf-trivial-subtype-top, R-state wf, fpf-single wf, top wf, fpf-join wf, id-deq wf, fpf-dom wf, assert wf, Id wf, R-compat-Rplus-sq, R-da wf, ma-valtype wf, R-base-recognize wf, R-compat-symmetry